<html>
<head><meta charset="utf-8"><title>Datalog and incremental SMT solving · t-compiler/wg-polonius · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/index.html">t-compiler/wg-polonius</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving.html">Datalog and incremental SMT solving</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="206607018"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Datalog%20and%20incremental%20SMT%20solving/near/206607018" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Amanda Stjerna <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving.html#206607018">(Aug 11 2020 at 17:47)</a>:</h4>
<p><a href="https://cs.pomona.edu/~michael/papers/iclp2020_extabs.pdf">This might be relevant to the Chalk integration</a>?</p>



<a name="206630073"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Datalog%20and%20incremental%20SMT%20solving/near/206630073" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving.html#206630073">(Aug 11 2020 at 20:55)</a>:</h4>
<p>is that a poster ? the complete Formulog paper seemed bigger when I saw it a couple days ago</p>



<a name="206630238"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Datalog%20and%20incremental%20SMT%20solving/near/206630238" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving.html#206630238">(Aug 11 2020 at 20:56)</a>:</h4>
<p>but I think SMT solvers seem unlikely to land in rustc :)</p>



<a name="206630446"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Datalog%20and%20incremental%20SMT%20solving/near/206630446" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving.html#206630446">(Aug 11 2020 at 20:58)</a>:</h4>
<p>but just reading the refinement type checker as one of the examples in the paper had me make this face: <span aria-label="heart eyes" class="emoji emoji-1f60d" role="img" title="heart eyes">:heart_eyes:</span></p>



<a name="206807290"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Datalog%20and%20incremental%20SMT%20solving/near/206807290" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Amanda Stjerna <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving.html#206807290">(Aug 13 2020 at 12:14)</a>:</h4>
<p>I didn't read it yet, but perhaps I should :)</p>



<a name="206807334"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Datalog%20and%20incremental%20SMT%20solving/near/206807334" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Amanda Stjerna <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving.html#206807334">(Aug 13 2020 at 12:14)</a>:</h4>
<p>I have...a large stack of papers to read, to say the least</p>



<a name="206912530"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Datalog%20and%20incremental%20SMT%20solving/near/206912530" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving.html#206912530">(Aug 14 2020 at 09:36)</a>:</h4>
<p><span class="user-mention silent" data-user-id="204115">Albin Stjerna</span> <a href="#narrow/stream/186049-t-compiler.2Fwg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving/near/206807334">said</a>:</p>
<blockquote>
<p>I have...a large stack of papers to read, to say the least</p>
</blockquote>
<p>I know that feeling. my "papers to read" folder has a subfolder "more relevant than others" and even that subfolder has too many papers in it...</p>



<a name="206950516"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Datalog%20and%20incremental%20SMT%20solving/near/206950516" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving.html#206950516">(Aug 14 2020 at 16:48)</a>:</h4>
<p>I have a lot of papers on my phone that I read while traveling to and from university.</p>



<a name="207076128"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Datalog%20and%20incremental%20SMT%20solving/near/207076128" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving.html#207076128">(Aug 16 2020 at 15:35)</a>:</h4>
<p><span class="user-mention silent" data-user-id="133247">bjorn3</span> <a href="#narrow/stream/186049-t-compiler.2Fwg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving/near/206950516">said</a>:</p>
<blockquote>
<p>I have a lot of papers on my phone that I read while traveling to and from university.</p>
</blockquote>
<p>Unfortunately, the trip from my bed to my desk is too short to read even a sentence…</p>



<a name="207077103"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Datalog%20and%20incremental%20SMT%20solving/near/207077103" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving.html#207077103">(Aug 16 2020 at 16:02)</a>:</h4>
<p>Since the pandemic I haven't read much papers myself either.</p>



<a name="207250815"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Datalog%20and%20incremental%20SMT%20solving/near/207250815" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Amanda Stjerna <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving.html#207250815">(Aug 18 2020 at 12:05)</a>:</h4>
<p>I...bike to university and don't think it would be a good idea to read while I do so</p>



<a name="207250820"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Datalog%20and%20incremental%20SMT%20solving/near/207250820" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Amanda Stjerna <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving.html#207250820">(Aug 18 2020 at 12:05)</a>:</h4>
<p>Also, it takes three minutes</p>



<a name="207359646"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Datalog%20and%20incremental%20SMT%20solving/near/207359646" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> namibj <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving.html#207359646">(Aug 19 2020 at 00:45)</a>:</h4>
<p><span class="user-mention" data-user-id="204115">@Albin Stjerna</span> <a href="#narrow/stream/186049-t-compiler.2Fwg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving/near/206807290">said</a>:</p>
<blockquote>
<p>I didn't read it yet, but perhaps I should :)</p>
</blockquote>
<p>Well, the last message of yours in here made me read it, it's thankfully quite short at 2.5 pages not counting references.</p>
<p>TL;DR: If you have a directed graph where each node has an SMT preposition <code>φ</code> attached to it, and want to efficiently find a path through the graph where the conjunction of the traversed node's SMT prepositions remains <code>SAT</code>, you just introduce one boolean variable <code>x</code> per graph node, rewrite the node's contribution to the SMT input to the implication <code>x =&gt; φ</code>, and then just ask the solver with <code>check-sat-assuming</code> (setting all those boolean variables based on whether the respective node is part of the path we're currently considering). They call this tactic CSA.</p>
<p>This lets the solver cache a lot, without really caring about the order in which we explore paths, and gives a speedup in 79 of 105 total experiments (over non-incremental baseline), being surpassed by a simple stack-based backtrace (named PP; using the assertion stack with <code>push</code> and <code>pop</code>) in 7 experiments.<br>
In 2 of the 7, CSA did not improve over baseline, while PP did. In the other 5 experiments, both improved on baseline, but PP did a better job.<br>
For symbolic execution, incremental was always better, and 12 of 18 cases were won by CSA.<br>
For refinement-types type-checking, CSA won for all 3 input programs (improving over baseline and delivering the best improvements).<br>
The random graph tests went mostly-good, with about half of the cases where incremental solving did not deliver an improvement used a logic combining linear integer arithmetic (_not_ bit vector logic) with arrays.</p>



<a name="207385850"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Datalog%20and%20incremental%20SMT%20solving/near/207385850" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Amanda Stjerna <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving.html#207385850">(Aug 19 2020 at 09:19)</a>:</h4>
<p>Wow, doing my work for me, thanks!</p>



<a name="208760388"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Datalog%20and%20incremental%20SMT%20solving/near/208760388" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving.html#208760388">(Sep 01 2020 at 23:08)</a>:</h4>
<p>this was also cute <a href="https://github.com/ekzhang/crepe">https://github.com/ekzhang/crepe</a></p>



<a name="218556838"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/186049-t-compiler/wg-polonius/topic/Datalog%20and%20incremental%20SMT%20solving/near/218556838" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Amanda Stjerna <a href="https://rust-lang.github.io/zulip_archive/stream/186049-t-compiler/wg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving.html#218556838">(Dec 02 2020 at 13:41)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116113">lqd</span> <a href="#narrow/stream/186049-t-compiler.2Fwg-polonius/topic/Datalog.20and.20incremental.20SMT.20solving/near/208760388">said</a>:</p>
<blockquote>
<p>this was also cute <a href="https://github.com/ekzhang/crepe">https://github.com/ekzhang/crepe</a></p>
</blockquote>
<p>Wow yes!</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>